from cheqed.core import theory, qterm, unification, side
from cheqed.core.sequent import Sequent

primitive = [
    'axiom',
    'left_permutation', 'right_permutation',
    'left_contraction', 'right_contraction',
    'left_weakening', 'right_weakening',
    'left_negation', 'right_negation',
    'left_disjunction', 'right_disjunction',
    'left_universal', 'right_universal',
    'left_substitution', 'right_substitution',
    'left_symmetry', 'right_symmetry',
    'left_beta', 'right_beta',
    ]

derived = []

__all__ = primitive + derived

def left_permutation(cursor, index):
    return cursor.apply('left_permutation', index)

def right_permutation(cursor, index):
    return cursor.apply('right_permutation', index)

def left_contraction(cursor):
    return cursor.apply('left_contraction')
    
def right_contraction(cursor):
    return cursor.apply('right_contraction')

def left_weakening(cursor):
    return cursor.apply('left_weakening')

def right_weakening(cursor):
    return cursor.apply('right_weakening')

def axiom(cursor):
    return cursor.apply('axiom')

def left_negation(cursor):
    return cursor.apply('left_negation')
    
def right_negation(cursor):
    return cursor.apply('right_negation')

def left_disjunction(cursor):
    return cursor.apply('left_disjunction')

def right_disjunction(cursor):
    return cursor.apply('right_disjunction')

def left_universal(cursor, witness):
    return cursor.apply('left_universal', witness)

def right_universal(cursor, witness):
    return cursor.apply('right_universal', witness)

def left_substitution(cursor):
    return cursor.apply('left_substitution')

def right_substitution(cursor):
    return cursor.apply('right_substitution')

def left_symmetry(cursor):
    return cursor.apply('left_symmetry')

def right_symmetry(cursor):
    return cursor.apply('right_symmetry')

def left_beta(cursor):
    return cursor.apply('left_beta')
    
def right_beta(cursor):
    return cursor.apply('right_beta')
